1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
/*!
# The Isotope Project
`isotope` is an experimental dependently typed language supporting borrow
checking, designed for use as an intermediate representation for building
verifiable systems languages.

`isotope` is composed of two languages: the "main" or "implementation" language,
and a "term" language. Expressions in the "main" language describe dependently
typed [RVSDG]s extended with lifetimes, which are given denotations in the
"term" language, which ignores low-level details such as lifetimes and
representation. In turn, the types of these expressions may depend only on
values in the "term" language, with programs, representations, and "main"
language types themselves values like any other. The "term" language itself is a
simplified implementation of the [Calculus of Constructions], inspired by
[Lean], extended with [Zombie]-like support for congruence-based normalization.

[RVSDG]: https://arxiv.org/abs/1912.05036
[Calculus of Constructions]: https://core.ac.uk/download/pdf/82038778.pdf
[Lean]: https://leanprover.github.io/
[Zombie]: https://www.seas.upenn.edu/~sweirich/papers/congruence-extended.pdf
*/
#![forbid(missing_debug_implementations, missing_docs, unsafe_code)]

pub mod ast;
pub mod builder;
pub mod ctx;
pub mod error;
pub mod primitive;
pub mod program;
pub mod repr;
pub mod term;
pub mod typing;
pub mod utils;

pub use error::Error;

/// Commonly used items
pub mod prelude {
    use crate::*;
    pub use ctx::{
        cons::ConsCtx,
        eq::{DisjointSetCtx, Structural, TermEqCtx, TermEqCtxEdit, TermEqCtxMut, Typed, Untyped},
        eval::{NormalCfg, Reduce, ReduceUntil, ReductionConfig},
        subst::{EvalCtx, Shift, SubstCtx, SubstSlice, SubstVec},
        ty::{BinaryCtx, Trivial, TrivialCons, TyCtxMut, TRIVIAL},
        StandardCtx,
    };
    pub use program::NodeIx;
    pub use term::{
        dynamic::{DynamicTerm, DynamicValue},
        flags::{AtomicTyckFlags, TyckFlag, TyckFlags},
        weak::WeakId,
        Annotation, AnnotationLike, AnnotationRef, App, Case, Cons, Enum, Form, HasDependencies,
        Id, Lambda, OptionalValue, Pi, Refl, Substitute, Term, TermEq, TermId, Typecheck, Universe,
        UniverseTerm, Value, Var, VarFilter, Variant,
    };
}

use prelude::*;

// Common imports
use ahash::AHasher;
use ctx::ty::MapTyCtx;
use enum_iterator::IntoEnumIterator;
use lazy_static::lazy_static;
use log::*;
use primitive::logical::*;
use smallvec::{smallvec, SmallVec};
use smol_str::SmolStr;
use std::any::Any;
use std::borrow::Borrow;
use std::borrow::Cow;
use std::cmp::Ordering;
use std::cmp::Ordering::*;
use std::convert::TryFrom;
use std::fmt::{self, Debug, Display, Formatter};
use std::hash::{BuildHasherDefault, Hash, Hasher};
use std::ops::*;
use std::sync::atomic::Ordering::*;
use std::sync::{Arc, Weak};
use term::flags::*;
use term::Code;
use utils::*;
use TyckFlag::*;